The Brazilian Symposium on Formal Methods (SBMF) is a scientific event that has been held annually since 1998. The 27th edition of SBMF will take place in 2024 in Vitória, the capital of Espírito Santo. SBMF courses and lectures are dedicated to disseminating recent advances in the field of formal methods. The technical sessions of SBMF foresee the presentation of unpublished works that make clear and significant contributions to the state of the art in the theory and practice of formal methods.
The main topics discussed at SBMF include:
Formal aspects of specification languages and theoretical foundations, such as the development of
new
domain-specific languages, the formalization of existing languages, and the study of the foundations
of
software engineering.
Formal aspects of systems development, such as the application of formal methods to the development
of
cyber-physical systems, embedded systems, and software-intensive systems.
Verification and validation, such as the formal verification of the correctness of software systems,
the
model checking of the requirements of software systems, and the fuzz testing of software systems.
Formal verification of neural networks, such as the application of formal methods to the
verification of
the correctness of deep learning models.
Self-formalization and formal aspects in practice, such as the automation of formal methods, the use
of
formal methods in industrial settings, and the teaching of formal methods.
Previous SBMF proceedings on https://link.springer.com/conference/sbmf
About the speaker: Julien Deantoni is a Professor at the Université Côte d'Azur and a researcher with the I3S/INRIA KAIROS team. His research focuses on the development of domain-specific languages (DSLs), particularly in the context of modeling and simulation of complex systems, behavioral semantics, and concurrent system coordination. He has contributed significantly to the development of tools such as TimeSquare, which allows for the specification and analysis of logical time constraints using the Clock Constraint Specification Language (CCSL). Julien has led various European and national research projects, including work on co-simulation frameworks for cyber-physical systems. His teaching covers a wide range of topics, including finite state machines, C++ programming, and embedded systems.
About the speaker: Marcel Vinicius Medeiros Oliveira is a Full Professor at the Department of Informatics and Applied Mathematics at the Federal University of Rio Grande do Norte (UFRN). He holds a Ph.D. in Computer Science from the University of York, England, and specializes in Formal Methods, with research focusing on refinement calculus, concurrency, formal language semantics, and code synthesis from formal specifications. Marcel is also a member of various academic committees, including the National Institute for Software Engineering, and serves as Coordinator of Technical Courses at UFRN’s Digital Metropolis Institute. His teaching covers Databases, Logic Applied to Software Engineering, and Formal Methods.
In deductive verification and software model checking, dealing with certain language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. This applies, in particular, to the concept of extended quantifiers found in specification languages like JML and ACSL. Extended quantifiers can be used to compute, among others, the maximum element or the sum of elements of an array and are frequently used in specifications, but tend to be difficult to support in verification tools. In the talk, I will present our ongoing research on how to automatically transform programs with such complicated operators to equivalent programs not containing the operators, and to reason about the correctness of those simpler programs instead. We apply our framework to cover the different kinds of extended quantifiers, which we formalize as monoid homomorphisms. Our approach is generic, however, and can be applied to describe a wide range of program transformations. The presentation is based on joint work with Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Marten Voorberg.
The line up of Industrial Talks will be available soon.
| Paper submission deadline†‡ | 18th August, 2024 5th July, 2024 |
| Acceptance notice | 23th September, 2024 6th September, 2024 |
| Camera-ready copy deadline† | 13th October, 2024 11th October, 2024 |
| SBMF 2024 | 4th—6th December, 2024 |
† All deadlines are until midnight of the specified date Anywhere on Earth (AoE).
‡ This is the final submission deadline and there will be no further extensions.
It is recommended to carefully read the information below to know the conditions and deadlines related to the registration. All registration fees are in Brazilian reais (R$/BRL).
| Dates | Category | SBMF | SBMF + SBC membership |
|---|---|---|---|
| 12/Aug - 29/Sep | Undergraduate Student – SBC Member | R$ 63,00 | R$ 94,00 |
| Undergraduate Student – non SBC Member | R$ 101,00 | R$ 94,00 | |
| Graduate Student – SBC Member | R$ 118,00 | R$ 243,00 | |
| Graduate Student – non SBC Member | R$ 255,00 | R$ 243,00 | |
| Basic Education Teacher – SBC Member | R$ 165,00 | R$ 290,00 | |
| Basic Education Teacher – non SBC Member | R$ 307,00 | R$ 290,00 | |
| Professional – SBC Member | R$ 211,00 | R$ 567,00 | |
| Professional – non SBC Member | R$ 589,00 | R$ 567,00 | |
| 30/Sep - 03/Nov | Undergraduate Student – SBC Member | R$ 88,00 | R$ 119,00 |
| Undergraduate Student – non SBC Member | R$ 128,00 | R$ 119,00 | |
| Graduate Student – SBC Member | R$ 134,00 | R$ 259,00 | |
| Graduate Student – non SBC Member | R$ 273,00 | R$ 259,00 | |
| Basic Education Teacher – SBC Member | R$ 180,00 | R$ 305,00 | |
| Basic Education Teacher – non SBC Member | R$ 323,00 | R$ 305,00 | |
| Professional – SBC Member | R$ 227,00 | R$ 583,00 | |
| Professional – non SBC Member | R$ 606,00 | R$ 583,00 | |
| 04/Nov - 06/Dec | Undergraduate Student – SBC Member | R$ 103,00 | R$ 134,00 |
| Undergraduate Student – non SBC Member | R$ 145,00 | R$ 134,00 | |
| Graduate Student – SBC Member | R$ 149,00 | R$ 274,00 | |
| Graduate Student – non SBC Member | R$ 289,00 | R$ 274,00 | |
| Basic Education Teacher – SBC Member | R$ 196,00 | R$ 321,00 | |
| Basic Education Teacher – non SBC Member | R$ 341,00 | R$ 321,00 | |
| Professional – SBC Member | R$ 237,00 | R$ 593,00 | |
| Professional – non SBC Member | R$ 617,00 | R$ 593,00 |
Non-SBC members or members with an annual fee that is about to expire can join or renew their membership along with their registration, choosing the COMBO categories with a discount on the registration fee.
The COMBO categories are the most advantageous option for non-SBC members, as the registration fees are lower than the categories without combo and include SBC membership.
Visit the SBC website and see why you should become a member.
Becoming a member of SBC is a way to make SBC even stronger to represent our area of work with the various sectors. How about becoming part of our Community?
Some exclusive member benefits:
Payment of enrollments can be made by means of bank slip, credit card, debit in Banco do Brasil account, purchase order or invoice.
Enrollments can be made until the last day of the event, however payments by debit and bill will be accepted until 2nd of December.
Enrollments by purchase order or invoice:
The participant must access the enrollment system and register, selecting the payment method "purchase order" or "invoice" and clicking on pay. The system will provide the information necessary for the enrollment to be confirmed.
Registration for SBMF authors. Papers accepted to SBMF will be published in a volume of LNCS. At least one author (professional or student) of each accepted paper must be registered for SBMF 2024. Authors can not use the registration benefits (exemption or 50% discount) granted by SBC to affiliated institutions. The author registration must be paid until November 11th, 2024.
We invite submissions of papers with a strong emphasis on formal methods, whether practical or theoretical, in the following categories:
The page limits exclude references and appendices.
Contributions should not be simultaneously submitted for publication elsewhere. They should be written in English, and prepared using Springer’s Lecture Notes in Computer Science (LNCS) format. Springer’s proceedings LaTeX templates are available in Overleaf. More information is available at the following link: https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines
Papers should present unpublished and original work that has a clear contribution to the state-of-the-art on the theory and practice of formal methods. Papers will be judged by at least three reviewers on the basis of originality, relevance, technical soundness and presentation quality and should contain sound theoretical or practical results. Industry papers should emphasize the practical application of formal methods or report on open challenges.
Submissions should be made via this link: https://easychair.org/conferences/?conf=sbmf2024
Session Chair: TBD
Session Chair: TBD
Session Chair: TBD
Session Chair: TBD
Presentation Durations:
| Time | Tuesday (2024-12-03) | Wednesday (2024-12-04) | Thursday (2024-12-05) | Friday (2024-12-06) |
|---|---|---|---|---|
| 08:30 | Registration Ifes Serra, Entrance hall | Registration Innovation City, Entrance hall | Registration Innovation City, Entrance hall | Registration Innovation City, Entrance hall |
| 09:00 | ETMF Opening Cerimony Ifes Serra, Auditorium | Poster Session / Meet and Greet Innovation City, Entrance hall | Keynote 2 Innovation City, Conference room | Keynote 3 Innovation City, Conference room |
| 09:30 | ETMF – Minicourse 1 Ifes Serra, Block 9/Lab. 903 | |||
| 10:00 | Coffee Break Innovation City, Living area | |||
| 10:30 | Coffee Break Ifes Serra, Block 9 living area | BSB Keynote Innovation City, Conference room To be confirmed. | Coffee Break Innovation City, Living area | Coffee Break Innovation City, Living area |
| 11:00 | ETMF – Minicourse 1 Ifes Serra, Block 9/Lab. 903 | Technical Session #2 Innovation City, Conference room | Industrial Talk Innovation City, Conference room | |
| 11:30 | Lunch | |||
| 12:00 | ||||
| 12:30 | Lunch | Lunch | Lunch | |
| 13:00 | ||||
| 13:30 | Registration Innovation City, Entrance hall | |||
| 14:00 | SBMF Opening Cerimony Innovation City, Conference room | |||
| 14:30 | ETMF – Minicourse 2 Ifes Serra, Block 9/Lab. 903 | Keynote 1 Innovation City, Conference room | Technical Session #3 Innovation City, Conference room | Technical Session #4 Innovation City, Conference room |
| 15:00 | ||||
| 15:30 | ||||
| 16:00 | Coffee Break Ifes Serra, Block 9 living area | Coffee Break Innovation City, Living area | Coffee Break Innovation City, Living area | SBMF Closing Cerimony Innovation City, Conference room |
| 16:30 | ETMF – Minicourse 3 Ifes Serra, Block 9/Lab. 903 | Technical Session #1 Innovation City, Conference room | Discussion Panel Innovation City, Conference room | |
| 17:00 | ||||
| 17:30 | ETMF Closing Cerimony Ifes Serra, Auditorium | CEFM Meeting Innovation City, Conference room | ||
| 18:00 | ||||
| 18:30 | ||||
| 19:00~19:30 | ||||
| 20:00 | Conference Dinner TBD | |||
| 20:30 | ||||
| 21:00 | ||||
| 21:30 | ||||
| 22:00 | ||||
| 22:30 |
Vitória, the capital of Espírito Santo, located in the Southeast
region of Brazil, is known for its beautiful beaches, historical
heritage, and strong economy. The city is a major financial,
corporate, research, technology, entertainment, and commercial
center in Brazil. Situated on an island, Vitória is famous for the
combination of its natural beauty with a vibrant urban life.
Hosting the 27th Brazilian Symposium on Formal Methods (SBMF 2024)
is the Graduate Program in Applied Computing (PPComp) at the Serra
Campus of the Federal Institute of
Espírito Santo (Ifes). Ifes is known for its excellence in
technical and higher education, offering a wide range of programs
across various fields of knowledge. PPComp, in particular, stands
out for its contribution to research and innovation in the field of
Applied Computing, being a pillar in the training of highly
qualified professionals and in conducting research that meets the
contemporary demands of society and the market.
Launched in 2019, PPComp is a young program that actively seeks to
consolidate itself as a center of excellence in its area. With a
firm commitment to the quality of education and research, the
program is committed to significantly contributing to the
advancement of applied computing, developing a solid foundation to
become a benchmark in the future, both regionally and nationally.
Moreover, the program's faculty have been actively collaborating
with local companies on research and technological development
projects, strengthening the bridge between academia and the
industrial sector, and contributing to the region's economic and
technological development.
The 27th SBMF will be hosted at the "Cidade da Inovação" (Innovation City) of Ifes, a hub designed to foster transformative solutions for sustainable development through collaboration with governmental bodies, the industrial sector, and civil society. Situated in the Jardim da Penha neighborhood of Vitória, in the premises formerly known as the IBC Sheds, this space now houses the Vitória Innovation Hub (PEIF-IFES), focusing on research and innovation in metallurgy, materials, and AI, alongside the regional office of the National Institute of Industrial Property (INPI).
The ambition is for this location to not only serve as a physical site for innovation and collaboration but to also act as a platform connecting the Ifes community, local society, and the productive sector globally.
Here are some hotel recommendations in the city of Vitória, catering to various preferences. For attendees seeking convenience, there are accommodations near the "Cidade da Inovação". For those looking for value, several budget-friendly options are available throughout the city.
ibis Vitoria Praia de Camburi
Av. Dante Michelini, 791 - Praia De Camburi, Vitória - ES, 29060-235
Telefone: +55 (27) 3203-5450
Vitória Praia Hotel
Av. Dante Michelini, 1057 - Jardim da Penha, Vitória - ES, 29060-235
Telefone: +55 (27) 3010-5500
Hotel Sol da Praia
Av. Dante Michelini, 877 - Jardim da Penha, Vitória - ES, 29065-050
Telefone: +55 (27) 2127-1500
Alameda Vitória Hotel
Av. Dante Michelini, 585 - Jardim da Penha, Vitória - ES, 29060-235
Telefone: +55 (27) 3204-6600
Ibis Budget Vitoria
Av. Nossa Sra. da Penha, 1993 - Bela Vista, Vitória - ES, 29056-075
Telefone: +55 (27) 3205-6155
Hotel Minuano
Avenida Dantas Micheline, 337 - Camburi, Vitória - ES, 29060-235
Telefone: +55 (27) 2121-7877
Ibis Vitoria Aeroporto
BR-101, Km 2 - S/2 - Bairro Carapina, Serra - ES, 29161-793
Telefone: +55 (27) 3041-4900
